i:Id, k:Knd. hasloc(k;i)  (isrcv(k)  destination(lnk(k)) = i) 

latex

Definitions	t  T, True, P  Q, x:A. B(x), destination(l), Id, Prop, False, A, P  Q, P & Q, P  Q, a = b, b, b, outl(x), IdLnk, 1of(t), x. t(x), Knd, lnk(k), isrcv(k), hasloc(k;i), P  Q, Dec(P)
Lemmas	decidable equal Id, Knd wf, pi1 wf, IdLnk wf, false wf, iff functionality wrt iff, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bnot wf, assert wf, eq id wf, not wf, true wf, Id wf, ldst wf